es:ES, Cmd:Type, isupdate:(Cmd), In:AbsInterface(Cmd), Sys:AbsInterface(Top).
(E(In) r E(Sys))
 (f:sys-antecedent(es;Sys), a:E(Sys). should-forward(es; In; isupdate; f; a)  ) 

latex

Up	abstract chain replication
Definitions of Statement	should-forward(es; In; isupdate; f; a)
Definitions	s = t, t  T, x:AB(x), x:A. B(x), EState(T), a:A fp B(a), f(a), Id, , strong-subtype(A;B), P  Q, Type, EqDecider(T), Unit, left + right, IdLnk, x:A  B(x), EOrderAxioms(E; pred?; info), kindcase(k; a.f(a); l,t.g(l;t) ), Knd, loc(e), kind(e), Msg(M), type List, , val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val;time), r  s, e < e', , b, constant_function(f;A;B), SWellFounded(R(x;y)), , pred!(e;e'), x,y. t(x;y), <a, b>, A, pred(e), first(e), x. t(x), P & Q, Top, ES, AbsInterface(A), E(X), E, e c e', {x:A| B(x)} , sys-antecedent(es;Sys), let x,y = A in B(x;y), t.1, !Void(), False, e  X, loc(e), Atom$n, ff, inr x , tt, inl x , case b of inl(x) => s(x) | inr(y) => t(y), True, A c B, if b then t else f fi , X(e), P  Q, (x  l), should-forward(es; In; isupdate; f; a)
Lemmas	event system wf, es-interface-val wf2, es-interface-val wf, true wf, btrue wf, bfalse wf, es-is-interface wf, false wf, sys-antecedent wf, es-E-interface-subtype rel, es-loc wf, es-causle wf, es-E wf, es-interface wf, es-E-interface wf, deq wf, EOrderAxioms wf, IdLnk wf, Msg wf, unit wf, nat wf, val-axiom wf, qle wf, cless wf, bool wf, top wf, Knd wf, kindcase wf, constant function wf, assert wf, not wf, loc wf, pred! wf, strongwellfounded wf, member wf, rationals wf, Id wf, EState wf, subtype rel wf